(*
 * Copyright (c) 2009, Palle Raabjerg
 * All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are met:
 *
 *   * Redistributions of source code must retain the above copyright notice,
 *     this list of conditions and the following disclaimer.
 *   * Redistributions in binary form must reproduce the above copyright notice,
 *     this list of conditions and the following disclaimer in the documentation
 *     and/or other materials provided with the distribution.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
 * AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
 * IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE
 * ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE
 * LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR
 * CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF
 * SUBSTITUTE GOODS OR SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS
 * INTERRUPTION) HOWEVER CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN
 * CONTRACT, STRICT LIABILITY, OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE)
 * ARISING IN ANY WAY OUT OF THE USE OF THIS SOFTWARE, EVEN IF ADVISED OF THE
 * POSSIBILITY OF SUCH DAMAGE.
 *)

let terms_of_terms ?(quotes = true) termlist =
  List.map (fun spiterm ->
	      match spiterm with
		| Spitree.Var(x) -> Alfp.Var(x)
		| Spitree.SpiMsg(msg) ->
		    if quotes then
		      Alfp.Const("\"" ^ (Spitree.string_of_msg_altsyntax msg) ^ "\"")
		    else
		      Alfp.Const(Spitree.string_of_msg_altsyntax msg)
	   ) termlist;;

let cpred_of_lit (rel, termlist) =
  Alfp.CPredicate(rel, (terms_of_terms termlist));;
let ppred_of_lit (rel, termlist) =
  Alfp.PPredicate(rel, (terms_of_terms termlist));;
let conj_of_ppreds literals =
  List.fold_left (fun ppred litfromlist ->
		    Alfp.PConjunction(ppred, ppred_of_lit litfromlist)
		 ) (ppred_of_lit (List.hd literals)) (List.tl literals)

let alfp_of_dat datprog =
  let clauses =
    List.map (fun hornclause ->
		if List.length hornclause = 1 then
		  let literal = List.hd hornclause in
		    cpred_of_lit literal
		else
		  let literal = List.hd hornclause in
		  let litlist = List.tl hornclause in
		  let clpred = cpred_of_lit literal in
		  let conj = conj_of_ppreds litlist in
		  let freevars = Alfp.freevars_in_pre conj in
		  let hornclause = Alfp.Leadsto(conj, clpred) in
		    Alfp.SSet.fold (fun var clause ->
				      Alfp.Forall(var, clause)
				   ) freevars hornclause
	     ) datprog
  in
    List.fold_left (fun cl clfromlist ->
		      Alfp.CConjunction(cl, clfromlist)
		   ) (List.hd clauses) (List.tl clauses);;

(*exception NotResultConjunction of string;;
let rec list_of_resultconjunction ccon =
  match ccon with
    | Alfp.CConjunction(cl1, cl2) ->
	let predlist1 = list_of_resultconjunction cl1 in
	let predlist2 = list_of_resultconjunction cl2 in
	  (List.append predlist1 predlist2)
    | Alfp.CPredicate(_, _) ->
	[ccon]
    | _ -> raise (NotResultConjunction "Must be a conjunction of CPredicates, as formed by the result of the Succinct Solver");;*)

exception IllegalHornClause of string;;
let clauses_to_literals datprog =
  List.map (fun clause ->
	      if List.length clause = 1 then
		List.hd clause
	      else
		raise (IllegalHornClause "Expected fact, but got a Horn Clause")
	   ) datprog;;

(*exception ThisIsABug of string;;*)
exception QueryFail of Spitree.datalog*Spitree.hclause;;
let querydat datprog queries ssolverheap =
  let alfpclause = alfp_of_dat datprog in
  let deducedclause = Ssolver.deducible_facts alfpclause ssolverheap
  in
    (*print_endline ("Program:\n" ^ (Alfp.string_of_cl alfpclause));*)
(*    List.iter (fun cpred ->
		 print_endline (Alfp.string_of_cl cpred)
	      ) deducedclause;*)
    if
      (List.for_all (fun query ->
		       let cpred_of_lit_mod (rel, termlist) =
			 Alfp.CPredicate(rel, (terms_of_terms ~quotes:false termlist)) in
		       let query_alfp = cpred_of_lit_mod query in
			 (*print_endline ("Query: " ^ (Alfp.string_of_cl query_alfp));*)
			 List.mem query_alfp deducedclause) queries)
    then true else
      raise (QueryFail (datprog, queries))
;;

(*let massquery datprog querylist ssolverheap =
  List.for_all (fun query ->
		  querydat datprog query ssolverheap
	       ) querylist;;*)

(*let infile = "datsamples/fklub.dat";;
let filechan = open_in infile;;
let lexbuf = Lexing.from_channel filechan;;

let datprog = Spiparser.dprogram Spilexer.spi_tokens lexbuf;;
let alfp = alfp_of_dat datprog;;
let query:Spitree.literal = ("factivity", [Spitree.SpiMsg(Spitree.Name("palle"))]);;
let res = querydat datprog query "ssolver/heap";; *)
